Motivation for this change

This generalizes bigcupT_measurable_ratto any choiceType whose whole set is countable.
I didn't prove a version with countType because I didn't manage to generalize the
quasi_canonical machinery. Anyway, that doesn't make the lemma less general. @CohenCyril

Checklist

• added corresponding entries in CHANGELOG_UNRELEASED.md

• added corresponding documentation in the headers

Reference: How to document

Reminder to reviewers

• Read this Checklist
• Put a milestone if possible
• Check labels